home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / fms_2.06.0 < prev    next >
Text File  |  1992-04-03  |  6KB  |  175 lines
  1. %%% FMS 
  2. %%% version 2.03.4 (based on fms_18.4)
  3. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  4. %%%     are visible externally -- changes to comments, predicate names, and
  5. %%%     variable names are not incorporated
  6. %%% version 2.05.3
  7. %%%   added support for Quintus Prolog
  8. %%% version 2.06.0
  9. %%%   added bug fixes from Shie-Jue
  10. %%%
  11. %%% The calculation of fully matched subset is very expensive, 
  12. %%% so we need to keep the number of clauses small. 
  13. %%% Hyper-matching is much better than matching in this sense.
  14. %%%
  15. %%% This algorithm is a little bit tricky. Fisrtly, we create in_fms set.
  16. %%% Secondly, we construct a link list for each in_fms. The link
  17. %%% list looks like:
  18. %%%    mref = link(F,[L1,L2,...,Ln])
  19. %%% F is the corresponding in_fms. Li is the link list for literal i in
  20. %%% in_fms. Each Li records the pointers to in_fms which has a mate of this
  21. %%% literal. Thirdly, we remove the non-fully matched clauses iteratively.
  22. %%%
  23. %%% In this version, we don't assert mref into the database, but we
  24. %%% put them in a list since they don't have any variables so prolog
  25. %%% won't complain a list with too many variables.
  26. %%%
  27. %%% User can choose either real fully matched subset or virtual fully 
  28. %%% matched subset is calculated. 
  29. %%% Virtual fully matched subset is used as default since we have a
  30. %%% very fast propositional calculus prover.
  31. %%% Duplicate removing is done for neither case.
  32. %%%
  33.  
  34.      compute_fms(FMS) :-
  35.     realfls,
  36.     cputime(TT1),
  37.     const_list(Clist),
  38.     tr_form(Clist),            % transform to economical form.
  39.     create_r(MRefs1),        % create link lists.
  40.     remove_clauses(MRefs1,MRefs2),    % remove unlinked clauses.
  41.     find_fms(MRefs2,FMS),        % find ground fms.
  42.     abolish(in_fms,2),        % release memory.
  43.     abolish(db_erased,1),        % release memory.
  44.     cputime(TT6),
  45.     TT7 is TT6 -TT1,
  46.     write_line(5,'Computing FLS(s): ',TT7),
  47.     !.
  48.      compute_fms(FMS) :-
  49.     cputime(TT1),
  50.     bagof1(X,grfclause(X),FMS),
  51.     cputime(TT2),
  52.     TT3 is TT2 - TT1,
  53.     write_line(5,'Computing FLS(s): ',TT3), !.
  54.  
  55.      grfclause(X) :-
  56.     sent_C(cl(_,_,by(Cn1,V11,V11,V1,_),_,_,_,_,_,_)),
  57.     grf_list(V1),
  58.     X = Cn1.
  59.  
  60. %%% transform to simpler form: in_fms(F,Ref1).
  61.      tr_form(Clist) :-
  62.     clause(sent_C(cl(_,_,by(_,_,_,_,W1),_,_,_,_,_,_)),true,Ref1),
  63.     tr_form(Clist,W1,Ref1,F),
  64.     assertz(in_fms(F,Ref1)),
  65.     fail.
  66.      tr_form(_).
  67.  
  68.      tr_form(Clist,W1,Ref1,F) :- tr_form(Clist,W1,Ref1,1,F).
  69.      tr_form(Clist,[_|Ws1],Ref1,N1,[Ln2|Ls2]) :-
  70.     clause(sent_C(cl(_,_,by(Cn2,V21,V21,_,W2),_,_,_,_,_,_)),true,Ref1),
  71.     retrieve_N2(Cn2,W2,N1,Ln2,_,Wn2,_),
  72.     Wn2 = Clist,
  73.     N2 is N1 + 1, !,
  74.     tr_form(Clist,Ws1,Ref1,N2,Ls2).
  75.      tr_form(_,[],_,_,[]).
  76.  
  77. %%% create link lists.
  78.      create_r(MRefs1) :- 
  79.     bagof1(Z,(Y,Z)^in_fms(Y,Z),Refs1),
  80.     create_r(Refs1,Refs1,MRefs1).
  81.  
  82.      create_r([Ref1|Refs1],Rin,[MRef1|MRefs1]) :-     
  83.     create_r2(Ref1,Rin,MRef1),
  84.     !,
  85.     create_r(Refs1,Rin,MRefs1).
  86.      create_r([],_,[]).
  87.  
  88.      create_r2(Ref1,Rin,link(Ref1,Links)) :-
  89.     clause(in_fms(Cg1,_),true,Ref1),
  90.     create_r3(Cg1,Ref1,Rin,Links), !.
  91.  
  92.      create_r3([],_,_,[]).
  93.      create_r3([Lg1|Lgs1],Ref1,Rin,[Link|Links]) :-
  94.     negate(Lg1,NLg1),
  95.     create_r4(Rin,Ref1,NLg1,Link),    % R1 is reference list for one literal.
  96.     create_r3(Lgs1,Ref1,Rin,Links).
  97.  
  98.      create_r4([],_,_,[]).
  99.      create_r4([Ref1|Refs1],Ref1,NLg1,Link) :-
  100.     !, create_r4(Refs1,Ref1,NLg1,Link), !.
  101.      create_r4([Ref2|Refs1],Ref1,NLg1,Link) :-
  102.     clause(in_fms(Cg2,_),true,Ref2),
  103.     create_r5(NLg1,Cg2,Ref2,Link,Link2),
  104.     !,
  105.     create_r4(Refs1,Ref1,NLg1,Link2).
  106.      create_r4([_|Refs1],Ref1,NLg1,Link) :-
  107.     create_r4(Refs1,Ref1,NLg1,Link).
  108.  
  109.      create_r5(NLg1,[NLg1|_],Ref2,[Ref2|Link2],Link2) :-
  110.     !.                % red cut.
  111.      create_r5(NLg1,[_|Lgs1],Ref2,Link,Link2) :-
  112.     !, create_r5(NLg1,Lgs1,Ref2,Link,Link2).
  113.  
  114.  
  115. %%% REMOVE UNLINKING NODES
  116. %%%
  117. %%% There is a trick for remove_clauses. We assure that if a literal
  118. %%% has a link then it can be detected by only checking the first
  119. %%% pointer in the literal link list after the first time. The reason
  120. %%% is that we delete the erased pointers in the literal link list
  121. %%% as we check the link relationship.
  122. %%% Note that we don't delete all the erased in_fms in a literal link
  123. %%% list. All we do is deleting the erased in_fms in front of a non-
  124. %%% erased in_fms, then stop. This process is the by-product of the
  125. %%% assoc routine. This will save time because deleting
  126. %%% the erased in_fms after a non-erased in_fms doesn't do any good
  127. %%% for us, and furthermore it needs extra time to do it.
  128.  
  129.      remove_clauses(MRefs1,MRefs2) :-
  130.     iterate(MRefs1,ORefs1),
  131.     !,
  132.     remove_clauses(ORefs1,MRefs2).
  133.      remove_clauses(MRefs2,MRefs2).
  134.  
  135. %%% We want to make it most efficient. If a in_fms has been deleted, then
  136. %%% we start from the begining again since the deleted in_fms may cause the
  137. %%% previous in_fms's to be deleted. If the current in_fms has bot been deleted,
  138. %%% then we continue to check the following in_fms because start from the 
  139. %%% beginning will do nothing for the previous in_fms.
  140.  
  141.      iterate([link(Ref1,Links)|MRefs1],[link(Ref1,NLinks)|ORefs1]) :-
  142.     assoc(Links,NLinks), !,        % check the link relationship.
  143.     iterate(MRefs1,ORefs1).
  144.      iterate([link(Ref1,_)|MRefs1],MRefs1) :-
  145.     erase(Ref1),
  146.     assert(db_erased(Ref1)).
  147.  
  148.      assoc([Link|Links],[NLink|NLinks]) :-    
  149.                     % succeed if all literals have links,
  150.     assoc_1(Link,NLink), !,        % fail if one literal has no links.
  151.     assoc(Links,NLinks).
  152.      assoc([],[]).
  153.  
  154.      assoc_1([Link|Links],[Link|Links]) :-    
  155.     \+ db_erased(Link), !.        % red cut.
  156.      assoc_1([_|Links],NLink) :-
  157.     assoc_1(Links,NLink).
  158.  
  159. %%% FIND OUT FMS
  160. %%%
  161. %%% We don't delete the duplicates in FMS, since duplicating is not a problem
  162. %%% for PC-prover.
  163.      find_fms(MRefs1,FMS) :-
  164.     grf_list(Glist),
  165.     find_fms(MRefs1,Glist,FMS).
  166.  
  167.      find_fms([link(Ref1,_)|MRefs1],Glist,[Cn2|FMSs1]) :-            
  168.                     % ground fms set.
  169.     clause(in_fms(_,Ref2),true,Ref1),
  170.     clause(sent_C(cl(_,_,by(Cn2,V21,V21,Glist,_),_,_,_,_,_,_)),
  171.         true,Ref2),
  172.     !,
  173.     find_fms(MRefs1,Glist,FMSs1).
  174.      find_fms([],_,[]).
  175.